\begin{tabbing}
$\forall$$E$, $X_{1}$, $X_{2}$:Type, ${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)).
\\[0ex]WellFnd\{i\}($E$;$e$,${\it e'}$.$\neg$first(${\it e'}$) \& $e$ $=$ pred(${\it e'}$) $\in$ $E$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ loc(pred($e$)) $=$ loc($e$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:$E$. loc($e$) $=$ loc(${\it e'}$) $\in$ Id $\Rightarrow$ ${\it pred?}$($e$) $=$ ${\it pred?}$(${\it e'}$) $\Rightarrow$ $e$ $=$ ${\it e'}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]loc($e$) $=$ loc(${\it e'}$) $\in$ Id
\\[0ex]$\Rightarrow$ \=($e$ $\lambda$$e$,${\it e'}$. $\neg$first(${\it e'}$) \& $e$ $=$ pred(${\it e'}$)\^{}+ ${\it e'}$)\+
\\[0ex]$\vee$ $e$ $=$ ${\it e'}$
\\[0ex]$\vee$ (${\it e'}$ $\lambda$$e$,${\it e'}$. $\neg$first(${\it e'}$) \& $e$ $=$ pred(${\it e'}$)\^{}+ $e$))
\-\-
\end{tabbing}